T:Type, R:(TT), P:(T).
(x, y:T. (P(y) & R(x,y))  P(x))  (x, y:T. (R|P^+(x,y))  (R^+|P(x,y))) 

latex

Definitions	, Type, x:AB(x), x:A  B(x), x(s), P  Q, P & Q, P  Q, P  Q, x:A. B(x), f(a), R^+, R|P, R1 => R2, x f y, , rel_exp(T;R;n), , {x:A| B(x)} , A, False, Void, A  B, a < b, Dec(P), P  Q, left + right, #$n, s ~ t, s = t, t  T, , SQType(T), {T}, (i = j), x:A. B(x), , b, b, n+m, -n, n - m, Trans(T;x,y.E(x;y))
Lemmas	rel plus trans, assert wf, not wf, bnot wf, bool wf, eq int wf, assert of eq int, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, bool sq, eqtt to assert, bool cases, rel-rel-plus, decidable int equal, le wf, rel exp wf, rel-restriction wf, nat plus properties, nat plus wf, rel plus-of-restriction